## What

Statements were **declared** (`Stmt`/`stmt`) in both provers but had
**no typing rules** — so `progress`/`preservation` never saw them. This
adds a context-threading **statement typing judgment** and its core
metatheory, in **both** Lean (`WokeLang.lean`) and Coq (`WokeLang.v`),
at parity. It directly retires the AUDIT.md row *"Statements: declared,
no typing/exec."*

## Judgment (mutually inductive with the block form)

- `StmtWellTyped Γ s Γ'` — a single statement threads the type context
- `StmtsWellTyped Γ ss Γ'` — a block threads the context left-to-right

All nine forms: `varDecl` (extends the context), `assign` (requires a
prior declaration at the assigned type), `return`, `if`, `loop`,
`attempt`, `consent`, `expr`, `complain`. Compound statements are
**block-scoped** (they return the incoming context). This is the
statement-level analogue of the expression `has_type`/`HasType`.

## Metatheorems (all proved)

- `ctxDomSub_{refl,trans,extend}` — the context-domain preorder + the
extension fact
- `stmt_wellTyped_mono` / `stmts_wellTyped_mono` — **context
monotonicity**: a well-typed statement/block never undeclares a variable
- `stmts_wellTyped_append` — **sequencing composes**: typing one block
then another from the resulting context types their concatenation
- `stmts_wellTyped_example` — inhabitation smoke (`let x = 0; x`)

## Verification

- **Lean 4.30.0:** `lean WokeLang.lean` → exit 0, no warnings,
`sorry`-free.
- **Coq 8.18.0:** `coqc WokeLang.v` → exit 0; `Print Assumptions` on all
four statement lemmas reports **"Closed under the global context"** —
i.e. axiom-free (they don't even touch the classical-reals axioms the
float fragment needs).
- Purely **additive** (new §5b in each file); existing theorems
untouched.

## Method note

The single-statement metatheorems are non-recursive (blocks are scoped),
which breaks the mutual dependency; the block versions then go by
ordinary **induction on the list**, sidestepping a mutual-induction
scheme in both provers.

## Scope / next step (honest)

This is the **static** story (typing + structural metatheory). The
**dynamic** story — a statement execution relation + a store-typing
*preservation* theorem — is the natural follow-up. Its prerequisite is
generalising the expression `preservation`/`type_safety` to **open**
terms (non-empty context + a store-typing agreement), since
statement-embedded expressions reference declared variables and the
current expression proofs assume the empty context. This is recorded in
AUDIT.md ("Recommended next proof steps" #3).

🤖 Generated with [Claude Code](https://claude.com/claude-code)

https://claude.ai/code/session_013wg3Mtq2QFhYi4XVw1Z6z7

---
_Generated by [Claude
Code](https://claude.ai/code/session_013wg3Mtq2QFhYi4XVw1Z6z7)_

---------

Co-authored-by: Claude <noreply@anthropic.com>